(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const j2 Int)
(assert (not (distinct b c)))
(assert (<= 150 b d))
(assert (< d a))
(assert (< c j2))
(assert (or (= (+ (mod b a) d) (/ (* a) c)) (= (+ (* d a)) (+ (* c a) j2)) (= 0 (mod (* j2 a) c))))
(check-sat)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const j2 Int)
(assert (not (distinct b c)))
(assert (<= 150 b d))
(assert (< d a))
(assert (< c j2))
(assert (or (= (+ (mod b a) d) (/ (* a) c)) (= (+ (* d a)) (+ (* c a) j2)) (= 0 (mod (* j2 a) c))))
(check-sat)
